MAYBE 1.357 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:



↳ HASKELL
  ↳ BR

mainModule Main
  ((iterate :: (a  ->  a)  ->  a  ->  [a]) :: (a  ->  a)  ->  a  ->  [a])

module Main where
  import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule Main
  ((iterate :: (a  ->  a)  ->  a  ->  [a]) :: (a  ->  a)  ->  a  ->  [a])

module Main where
  import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
          ↳ Narrow

mainModule Main
  (iterate :: (a  ->  a)  ->  a  ->  [a])

module Main where
  import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ QDP
              ↳ NonTerminationProof
          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_iterate(vx3, ba) → new_iterate(vx3, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_iterate(vx3, ba) → new_iterate(vx3, ba)

The TRS R consists of the following rules:none


s = new_iterate(vx3, ba) evaluates to t =new_iterate(vx3, ba)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_iterate(vx3, ba) to new_iterate(vx3, ba).




Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
          ↳ Narrow
            ↳ QDP
              ↳ PisEmptyProof

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.